Nuprl Lemma : p-open-member_wf
11,40
postcript
pdf
p
:FinProbSpace,
C
:p-open(
p
),
s
:(
Outcome).
s
C
latex
Definitions
FinProbSpace
,
t
T
,
#$n
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
Outcome
,
{
x
:
A
|
B
(
x
)}
,
,
x
:
A
B
(
x
)
,
Type
,
A
B
,
S
T
,
P
&
Q
,
i
j
<
k
,
suptype(
S
;
T
)
,
<
a
,
b
>
,
f
(
a
)
,
x
:
A
B
(
x
)
,
,
s
=
t
,
,
x
:
A
.
B
(
x
)
,
s
C
,
p-open(
p
)
Lemmas
le
wf
,
nat
wf
,
p-outcome
wf
,
int
seg
wf
,
finite-prob-space
wf
origin
p:FinProbSpace, C:p-open(p), s:(
Outcome). s 
C 
p:FinProbSpace, C:p-open(p), s:(Outcome). s C Tx:A. B(x)
}B(x)
B
T j < k
B(x)
x:A. B(x) C